We present a case study of formal verification of full-wave rectifier foranalog and mixed signal designs. We have used the Checkmate tool from CMU [1],which is a public domain formal verification tool for hybrid systems. Due tothe restriction imposed by Checkmate it necessitates to make the changes in theCheckmate implementation to implement the complex and non-linear system.Full-wave rectifier has been implemented by using the Checkmate custom blocksand the Simulink blocks from MATLAB from Math works. After establishing therequired changes in the Checkmate implementation we are able to efficientlyverify the safety properties of the full-wave rectifier.
展开▼
